Step of Proof: fib_wf 11,40
Inference at * 1 0 
Iof proof for Lemma fib wf:



1. n : 
2. n1:. (n1 < n)  (fib(n1)  )
  fib(n)   
latex
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{4:n,
 by PERMUTE{7:n,
 by PERMUTE{5:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{14:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{18:n,
 by PERMUTE{21:n,
 by PERMUTE{19:n,
 by PERMUTE{22:n,
 by PERMUTE{23:n,
 by PERMUTE{24:n,
 by PERMUTE{25:n,
 by PERMUTE{26:n,
 by PERMUTE{19:n,
 by PERMUTE{27:n,
 by PERMUTE{20:n,
 by PERMUTE{28:n,
 by PERMUTE{29:n,
 by PERMUTE{30:n,
 by PERMUTE{31:n,
 by PERMUTE{32:n,
 by PERMUTE{33:n,
 by PERMUTE{30:n,
 by PERMUTE{34:n,
 by PERMUTE{31:n,
 by PERMUTE{23:n,
 by PERMUTE{35:n,
 by PERMUTE{36:n,
 by PERMUTE{37:n,
 by PERMUTE{38:n,
 by PERMUTE{32:n,
 by PERMUTE{39:n,
 by PERMUTE{33:n,
 by PERMUTE{24:n,
 by PERMUTE{40:n,
 by PERMUTE{41:n,
 by PERMUTE{37:n,
 by PERMUTE{42:n,
 by PERMUTE{43:n} 
latex

 1: .....wf..... NILNIL

 1:   ((n = 0) (n = 1))  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 3. ((n = 0) (n = 1)) = tt
 3:   (((n = 0) (n = 1)) = tt)  
 4: .....wf..... NILNIL

 4: 3. ((n = 0) (n = 1)) = tt
 4:   (((n = 0) (n = 1)))  
 5: .....wf..... NILNIL

 5: 3. ((n = 0) (n = 1)) = tt
 5:   ((n = 0)  (n = 1))  
 6: .....wf..... NILNIL

 6: 3. ((n = 0) (n = 1)) = tt
 6:   ((n = 0) (n = 1))  
 7: .....wf..... NILNIL

 7: 3. ((n = 0) (n = 1)) = tt
 7:   (((n = 0))  ((n = 1)))  
 8: .....wf..... NILNIL

 8: 3. ((n = 0) (n = 1)) = tt
 8:   (n = 0)  
 9: .....wf..... NILNIL

 9: 3. ((n = 0) (n = 1)) = tt
 9:   (n = 1)  
 10: .....wf..... NILNIL

 10: 3. ((n = 0) (n = 1)) = tt
 10:   ((n = 0))  
 11: .....wf..... NILNIL

 11: 3. ((n = 0) (n = 1)) = tt
 11:   (n = 0)  
 12: .....wf..... NILNIL

 12: 3. ((n = 0) (n = 1)) = tt
 12:   ((n = 1))  
 13: .....wf..... NILNIL

 13: 3. ((n = 0) (n = 1)) = tt
 13:   (n = 1)  
 14: .....wf..... NILNIL

 14: 3. ((n = 0) (n = 1)) = tt
 14:   n  
 15: .....wf..... NILNIL

 15: 3. ((n = 0) (n = 1)) = tt
 15:   0  
 16: .....wf..... NILNIL

 16: 3. ((n = 0) (n = 1)) = tt
 16:   1  
 17: .....truecase..... NILNIL

 17: 3. (n = 0)  (n = 1)
 17:   1  
 18: .....wf..... NILNIL

 18: 3. ((n = 0) (n = 1)) = ff
 18:   (((n = 0) (n = 1)) = ff)  
 19: .....wf..... NILNIL

 19: 3. ((n = 0) (n = 1)) = ff
 19:   ((((n = 0))  ((n = 1))))  
 20: .....wf..... NILNIL

 20: 3. ((n = 0) (n = 1)) = ff
 20:   (((n = 0)) & ((n = 1)))  
 21: .....wf..... NILNIL

 21: 3. ((n = 0) (n = 1)) = ff
 21:   ((((n = 0) (n = 1))))  
 22: .....wf..... NILNIL

 22: 3. ((n = 0) (n = 1)) = ff
 22:   ((n = 0) (n = 1))  
 23: .....wf..... NILNIL

 23: 3. ((n = 0) (n = 1)) = ff
 23:   (n = 0)  
 24: .....wf..... NILNIL

 24: 3. ((n = 0) (n = 1)) = ff
 24:   (n = 1)  
 25: .....antecedent..... NILNIL

 25: 3. ((n = 0) (n = 1)) = ff
 25:   True
 26: .....wf..... NILNIL

 26: 3. ((n = 0) (n = 1)) = ff
 26: 4. ((((n = 0) (n = 1)))) = ((((n = 0))  ((n = 1))))
 26:    = 
 27: .....wf..... NILNIL

 27: 3. ((n = 0) (n = 1)) = ff
 27:   ((((n = 0))) & (((n = 1))))  
 28: .....wf..... NILNIL

 28: 3. ((n = 0) (n = 1)) = ff
 28:   ((n = 0))  
 29: .....wf..... NILNIL

 29: 3. ((n = 0) (n = 1)) = ff
 29:   ((n = 1))  
 30: .....wf..... NILNIL

 30: 3. ((n = 0) (n = 1)) = ff
 30:   (((n = 0)))  
 31: .....wf..... NILNIL

 31: 3. ((n = 0) (n = 1)) = ff
 31:   ((n = 0))  
 32: .....wf..... NILNIL

 32: 3. ((n = 0) (n = 1)) = ff
 32:   (((n = 1)))  
 33: .....wf..... NILNIL

 33: 3. ((n = 0) (n = 1)) = ff
 33:   ((n = 1))  
 34: .....wf..... NILNIL

 34: 3. ((n = 0) (n = 1)) = ff
 34:   (((n = 0)))  
 35: .....wf..... NILNIL

 35: 3. ((n = 0) (n = 1)) = ff
 35:   ((n = 0))  
 36: .....wf..... NILNIL

 36: 3. ((n = 0) (n = 1)) = ff
 36:   (n = 0)  
 37: .....wf..... NILNIL

 37: 3. ((n = 0) (n = 1)) = ff
 37:   n  
 38: .....wf..... NILNIL

 38: 3. ((n = 0) (n = 1)) = ff
 38:   0  
 39: .....wf..... NILNIL

 39: 3. ((n = 0) (n = 1)) = ff
 39:   (((n = 1)))  
 40: .....wf..... NILNIL

 40: 3. ((n = 0) (n = 1)) = ff
 40:   ((n = 1))  
 41: .....wf..... NILNIL

 41: 3. ((n = 0) (n = 1)) = ff
 41:   (n = 1)  
 42: .....wf..... NILNIL

 42: 3. ((n = 0) (n = 1)) = ff
 42:   1  
 43: .....falsecase..... NILNIL

 43: 3. ((n = 0)) & ((n = 1))
 43:   fib(n - 1)+fib(n - 2)  
 .

Definitions{x:A| B(x)} , b, p  q, A, inr x , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), b, P  Q, , Ax, , inl x , left + right, x:AB(x), s = t, Type, n - m, n+m, #$n, (i = j), p q, x.A(x), f(a), a < b, , , Unit, , True, T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , Y, fib(n), t  T, P  Q, x:A. B(x)
Lemmasnot functionality wrt iff, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of eq int, or functionality wrt iff, assert of bor, eqtt to assert, iff transitivity

origin